package folexpr.compiler.visitors.h_removeforall;

import folexpr.compiler.CompilerConstants;
import folexpr.compiler.CompilerUtils;
import folexpr.compiler.visitors.CompilerVisitor;
import folexpr.compiler.visitors.VisitResult;

import folexpr.parser.syntaxtree.quantificazione;

/**
 * INTERMEDIATE  o COMPILING visitor
 * 
 * Ultimo step (8) della trasformazione in clausole:
 * Rimuove i quantificatori rimasti - tutti universali
 * 
 * Se trova un quantificatore esistenziale lancia un'exception ma continua comunque la visita
 * come se avesse incontrato un perogni ritornando la sua immagine senza la quantificazione.
 * 
 * Simboli non terminali maggiormente interessati:
 * quantificazione -> restituisce in out la sua immagine senza la quantificazione "forall <VAR>"
 * 
 * Ritorna un albero sintattico dello stesso tipo di quello che ha in input dal parser 
 * quindi one_line oppure fbf
 * 
 */

public class RemoveForallVisitor extends CompilerVisitor<Object>
{
	//////////////////////////////////////////////////////////////////////////////////////
	
	public RemoveForallVisitor()
	{
		super(CompilerConstants.REMOVE_FORALL);
		
		// override
		this.debug = CompilerConstants.LOG_REMOVE_FORALL_VISITOR;
	}
	
	/////////////////////////////////////////////////////////////////////////////////////
	
	@Override public VisitResult visit(quantificazione n, Object argu)
	{
		if (debug) System.out.println(CompilerUtils.indent(level,8)+"VISIT(" + n.getClass().getName() +") : INIZIO");
		VisitResult outerResult= new VisitResult();
		
		String quantificator = n.f0.accept(this,argu).getResultExpr();
		
		if (quantificator.equals(forallImage) || quantificator.equals(forallImage + " "))
				outerResult.setResultExpr( n.f2.accept(this,argu).getResultExpr() );
		else if (quantificator.equals(existsImage) || quantificator.equals(existsImage + " "))
		{
			//TODO classificare meglio le eccezioni
			try {
				throw new Exception("Arrivati a questo punto " +
						"non ci devono piu' essere delle quantificazioni esistenziali " +
						"perche' le ho eliminate al passo precedente di skolemizzazione.");
			} catch (Exception e) {
				e.printStackTrace();
				outerResult.setResultExpr( n.f2.accept(this,argu).getResultExpr() );
			}
		}
			
		if (debug) System.out.println("risultato:"+outerResult.getResultExpr()+".");
		if (debug) System.out.println(CompilerUtils.indent(level,8)+"VISIT(" + n.getClass().getName() +") : FINE");
		return outerResult;
	}

}

